[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

MASTERARBEIT

Titel der Masterarbeit

On Hilbert’s Tenth Problem over

Rings of Algebraic Integers

Verfasser

Tim Benedikt Herbstrith

angestrebter akademischer Grad

Master of Science (MSc.)

Wien, im Monat September 2018

Studienkennzahl lt. Studienblatt: A 033 821

Studienrichtung lt. Studienblatt: Mathematik

Betreuer: ao. Univ.-Prof. Mag. Dr. Ch. Baxa

[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

                   

         

                  

                 

       

https://github.com/tim6her/h10-over-rings-of-integers

[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

Vorwort

 



Abstract

 





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

Contents

1 Prerequisites and central notions 1

                           

                      

                      

                               

                                

                        

                     

                               

                        

   



                                

                               

                             

2 Hilbert’s tenth problem 55

                             

                           

                              

                                 

                                   

               

                              

                          

A Appendix 99

                             

                            

                                  



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

1 Prerequisites and central notions

               

                

                 

 

                

              

               

               



           









1.1 Prerequisites from computability theory

            

           

            



              

            

                  

             

           

               

            

                

          

                   

              

                

                 

         

1.1.1 Turing machines, problems, and decidability

            01 01





      01    



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

1 3

≅

↕

𝑥 = 101

≠

𝑦 = 011

↕

       

               

         

           



               

           





 

       

              

               

         

 







 







 



 







              

        



1 

          

      

101  011       

          

                 

               

                 

                    

          §             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

0 0 0 1

. . .

overflow

    

          _       

  

       §_01      

            

start



halt

  



    



      

 §     §

  §   

  

halt

 





halt

  

                

                 

               

                 

    

       §          

              

      

halt

          

 

                   

    0            

 0     

overow

   



overow

0

return

1

              

return

  

 1                  

    

overow

0          

               

 

               





                 

  



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

     

halt

         



start

  §       _     

         

§__

              

                 

 

§001_0__

                



01



 

      











        









§  





 

_ 

   











       

 















  











       

 

 









 



 

 



  

              

                   

 

start

              



halt

       

           

delta



state



state’







 

delta "state" b = ("state'", b', m)

             

               

     

delta "state" 1 = ("state'", b', m)

delta "state" b = ("state''", b'', m')

   







state’





  

state

1



state”









  

state

1





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

          

-- start by entering the "overflow" state ...

add1 "start" '§' = ("overflow", '§', 1 )

-- ... and stay in this state, as long as you read only '1'-s

add1 "overflow" '1' = ("overflow", '0', 1 )

-- if you read the first '0' or an empty cell replace it by '1'

-- and enter the "return" state to move the head to the first cell

add1 "overflow" '0' = ("return", '1', -1)

add1 "overflow" '_' = ("return", '1', -1)

-- we finish if we read '§' again or ...

add1 "return" '§' = ("halt", '§', 0 )

-- ... continue to move to the left and don't change the cell

-- content. Here `b` matches '0' or '1'

add1 "return" b = ("return", b , -1)

add1 _state _char = ("error", '_', 0 )

              

              



            

      

add1



start



halt



overow



return



error



add1



              

     

                 

           

error

     

add1



1101        

     

               

    

     1     0

     01



         

          

  01



       

  

              

      

                 

               



 https://www.haskell.org/onlinereport/haskell2010



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

1 1 0 1

. . .

start

 

start

§

overﬂow

§

1 1 0 1

. . .

overflow

 

overﬂow

1

overﬂow

1

0 1 0 1

. . .

overflow

 

overﬂow

1

overﬂow

1

0 0 0 1

. . .

overflow

 

overﬂow

0

return

1

0 0 1 1

. . .

return

 

return

1

return

1

0 0 1 1

. . .

return

 

return

1

return

1

0 0 1 1

. . .

return

 

return

§

halt

§

0 0 1 1

. . .

halt

 

halt

§

halt

§

      

add1

 1101



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                 

           







start



halt



reject

























 





            



start

















1













1  



reject

_ 











0













0  



reject

_ 











_





_  











reject

_  











                









     

























                   

               

                

         

       _            

    

                 

        

          







   

 

          1    

reject

   

     0  

           

       

 

reject

      

                

  

                 





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

   











 











     









 







  







       

  









    





















 

 



 





  

start



halt

  



  



     

      





start

§ 

halt

§  



    

     















              









 









   















start



halt



 















start



halt



   





start



halt























compose



             

 

















  











start





compose

  



 





halt











  











halt









start

  

compose

 









 







         



 

       





        

   

 11



-times

  



    





























1  

0

          

























  



            01



   





     



01





     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

          

-- start by entering the "check" state and ...

tally "start" '§' = ("check", '§', 1 )

-- ... stay in this state while reading only '1'-s

tally "check" '1' = ("check", '1', 1 )

-- on reading '_' accept the input and clear the tape ...

tally "check" '_' = ("accept", '_', -1)

tally "accept" '1' = ("accept", '_', -1)

-- ...except for cell c(1), where you write a '1'

tally "accept" '§' = ("accept", '§', 1 )

tally "accept" '_' = ("halt", '1', -1)

-- however, if you read a '0' first, reject the input

-- by moving to the end of the input string ...

tally "check" '0' = ("rejectMR", '0', 1 )

tally "rejectMR" '_' = ("reject", '_', -1)

tally "rejectMR" b = ("rejectMR", b, 1 ) -- `b` matches '0' or '1'

-- ... and clear the tape except for cell c(1) where you

-- write a '0'

tally "reject" '§' = ("reject", '§', 1 )

tally "reject" '_' = ("halt", '0', -1)

tally "reject" b = ("reject", '_', -1) -- `b` matches '0' or '1'

tally _state _char = ("error", '_', 0 )

                   

        



01







                  

         1         



tally



start



halt



check



reject



rejectMR



error



                 

       1         

 



    



   

  



            

               

             



  





0     

               

              

               





              



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

 























     















     

   







 



 





             

 





 11



-times

0 11



-times



                

    0      1      





    0     



         

    1       

        













































































01 













                  

               

 



              01

                 

               



    

        

                    

 §                   

                 

                     

                 

         

             

      



























      







    



     

             













                









           

  





  



            































     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

. . .

n−2

n−1

. . .

find non-empty

 The machine ﬁnds the ﬁrst non-empty cell.

. . .

n−2

n−1

. . .

shift left b

 The machine shifts the content of each cell one cell to the left …

. . .

n−1

. . .

shift left b

 … until it reaches the end of tape symbol §.

. . .

n−1

. . .

find __

 The machine ﬁnds two consecutive blank cells and starts over.

                

               

              

  



      



   

  













 





           



   

  0   



  

   



      



 

  

    



             

             

                

                

     

              

      











   

§ 



__ 



__





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

               

         











     

               

     

§ 



_







_







_





     



         

            



    

               

           

              

            

          

  

        

        

      



 

  

              

   1           1 

    

    



      1   1  

            



   

   

                

               

          

     







   

§















_

                 

                

                  

§







_

                

 

                  

               



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

            1

-- start by entering the "check" state

check1 "start" '§' = ("check", '§', 1 )

-- if you read a 1, check that the next cell is blank, and accept

check1 "check" '1' = ("check_blank", '1', 1 )

check1 "check_blank" '_' = ("accept", '_', -1)

-- if either of these conditions is not the case, reject

check1 "check" b = ("reject", b, 1 )

check1 "check_blank" b = ("reject", b, 1 )

-- accepting and rejecting actions

check1 "accept" 1 = ("halt", 1, -1)

check1 "reject" b = ("error", b, 1)

check1 _state _char = ("error", '_', 0 )

               

           







 







  

   



 

         

            



   

                

               

                   

                



  









 

           

   1           1   

   

             

     

           

                   

               

 

              



              



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

         10  01  

            

              



             

            1

                

          1      

       



     















10100



0



0



0



0



0





               

          1      0    

           

      



       

       





         











    

     



     





     











            

               1      

           



  



 





       0            

                

   



             

             1       

       

              1       

        



    

           



   

            











   

       1  0         



 

halt

 





1.1.2 Church-Turing thesis and the halting problem

               

              

            

   

             

  

               

      

             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                       

 

                

                 

                  

             

             

         

  

                  

                   

               

              

            

            

                

                 

             

             

      

               

    





1    

0      

         

                 

        



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

       



     

      0     





        

 



   

                

          





  



             

         

               

                 



   

               

      

  

   

         



    

     









       

                

                

             

      

    



    







   



 

   

        



  



    



  

    



          

           

 



   



            

         



  

  



   

        



       

 



      



 



     

               

          

        



   



    



 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                 

         



      



 

1.2 Prerequisites from model theory

               

             

                  

        

1.2.1 Formulae and models

              

              

             

                

               

              

      







     

                  

           

      



 





    



          

    



    



      

  



 

       

















        

     

      

      











      

     









1

e



      

1

 

    e    

       







01



      

   01  

             

               



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

  







         

          

   









    

   









     

   



    

    















   

           

            

                

            











 





        

   









1

e



         









1



e



  



   

1



 

  e



       



0  0 

        



  

          











0



1



  













     0



1



       

      



         



 

      









        





        



                 

  







          

  

      

    x

x

   

  









   









       

  x

x

x

x

1  



     

         

x

x

x

1

              





                  

               











  

        







[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

   







         

     x

x

      x

x

 

   







  x

x

  

  x

x

  















  









  x

x

x

   









      

  x

x

   

x

x





x

x







x

x



       



x

x







x

x

 

















































                  

                 

                

  

           



    

           









    



            

     

        0  1       



  x

  







  







  

   







  







 







       





 





       







    

            









               





1 1 1



-times

       

01 1 1



-times



   



















  















   

    

a 













 a                



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

 







    

m

m



 m

    



   





         





 













  







 



















     









  



     

             

  







        



    







  







 

    









      











               

   

         

  







     







  

                

  

       

  







      







 









  







   







   









                 

 

                



                 

         



   

     





 x

x

x

 x

x

x

1

 x

x

x

x

x

x

x

x

x

                 

                     



              x

x

x

     

 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

       

 x

 x

 x



 x

    x

 

       

             

            



     

        x

x

 x

       

     

               

              

         

  x

x

x

   x



 x

               x

x



      x

x

   

                

x

x

 















   









 











       

  







   







  







































  









      









  













































       







 







  

  







   







  







  













 













  x

x

x

x

  







    

  









                

       

                

 x



x

x

x

x

x

x

x



                   

                 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                  

               

x

x

x

x

x

x

x



           

                  

           

1.2.2 Morphisms, theories, and decidability

               

              

              

       

   







       

        

 



























     











 













 













    









 

 







  

         



   

       



       

    



  



           

 



         





       



       



         

 

              

       

    

        

                 

 

                 

     

  



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

              

      

             



    

   

x

x

e x



x

e x

x



x

x

x

x

x

x

x

x



x

x

x

1

e

x

x

1

x

e

             

    



   

          

x

x

0x

x

x

1

     

             

                 



 

  

 

  



    



       

 

            

               

        

                 

                

     

              

          

             

        

Th







     

        

H10







x

x

x

x

   





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

           

 

   



  











x

x













x

x







is atomic, and 



             

                

      



    

x

x

0x

x

x

1

       Th    







    

      Th

  x

x

1 0         

 



       Th



     

  Th





     









            

             

x

x

Ex

x

Ex

x

Ex

x



    x

    x

x

       Th





              

                  

         



      

     



          

 



            

               

















           

      



   c





  

                 

 







[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

        

















  



   

       

H10







x

x

x

x

   



      



     

        













x

x













x

x







is atomic, and 



        



     

       













there exists an atomic formula with

, or and 



   



     



     

                 

   

            





        



       









  P 



        



   



P 









     P  

H10     

     



          

 











           

    







    

         



















 























     



x

x



               

        

  P       P     



  

x

x

x

x





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

 



      



      

  







 











         





 





    









  













      







          

  



  

x

x

x

x

0

 x

x

         

  H10              

x

x





x

x





x

x



  



 







                 

  











 







































        







   

                  

                   

             

         





x













                

    









              

 x

   

-times











    

s 













 



     



x







































 



   



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

               

              

       

                 

    





x

x

0

         

        x



   0 1

              

       

s 









   



































    

            

  







  

              

     

H10

∗

(𝔄)

∃+

(𝔄)

Th(𝔄)

𝐷(𝔄)

H10(𝔄)

𝐷

∃+

(𝔄)

𝐷

𝑐

(𝔄)

                

                 

        









           Th



  

 H10



  



    H10



      



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                

   



            

          

H10

∗

(𝔄)

∃+

(𝔄)

Th(𝔄)

𝐷(𝔄)

H10(𝔄)

𝐷

∃+

(𝔄)

𝐷

𝑐

(𝔄)

𝒦

1.2.3 Computable structures and decidable models

                

              

               

             

              

                

      

               

          

               

                









             

        

   ar    

                  

            

     

              

        

             

   







            

            

        

                

  



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                 

                

     

               

            

             

           

             



                

   FC     R  

F

























        











R









  















        









 

C



     

              

   



   

          

           



 

 



      



  

            

   







  



  





        



  



     

    















 

















 



     









             



  

         



       

 













 



     













    















       



    

              

             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

           

  

                

   

        

        





      

      







     

           



      

  



           

              1 

            

   



            

 

                

 1               

               

11011

   0   1     1

           







 

  







      



        



  

   







  







     









                

            

          



  

           

         







       

            

          









 





















 























 







    





















 







[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

        





 

       



   





              

    

              

               

             

  

   



       



 

   







   

    



    



          

                

              

      



          

              

               

          

                

              

  



       



 



                  









         















  

         

















 



 



 















 



 



       

 









        



 



  

      

            



     

   



          

               

           



 

     



 



        

         0





0





  

c

n1





c





1







 c

        

              

               

     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

            



 

   H10 

    



          

     



  

x

x

x

x

  



 

       







    







 











  









             

 



 









  









      H10    

1.3 Prerequisites from number theory

1.3.1 Number ﬁelds and rings of algebraic integers

                 

               

                 

               

          





 



                

               

         







     

  







  







     









        







































    









 

            

                  

            

              

              

 



 











          





         



















[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

 

























       

               

                 





             

  



           

    



    

                 

              

 

            

                   



















    







          

                

    

                 

                

   

              

     

           

            

              

  

              

             











































              

           



 



    

       



      



 

    







































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

       







 







     

  















 













        

 

















 

            

            











































   







  







 



























































  

                

     

            

        

  



                

  



    

                

               

               



   

     



            

     



       

   



          

                

       







       

      



            

             

        



       

      







       

      



       

            



   



 

  







     



     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

    



         





 



   





       



      



   

   



 







  







    

  



            

   

                  

 



            

   



      



      





















  







   



         





              

     

            

     



      



 

        



       

      









  

               

   

               

  



  



     











      











           



    

            











   

     

              

                

 







        

 

















 















 

 



















            



 

               



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

  

            

    

                

         

             

         





     

 



  





 





         

         





     

               

               

          



     

             

             













 













                 

   



   



  



     

              

       



 



   



   

   



 



 



  

       



         





    



   



     



   

    





















  







          

      



       



 

            





          



    







     



 



          

 



             



















              

               

                   

         



      

       



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

        



      



 

     





    



            

           



   

            



  

1.3.2 Ideals of 



              

            



   

             

     



  











 



 



      

              

            











 



 









 







 











  















































     

            









  







           

        



      

                 

                   

     

                

                  



            



























































                     





              



 

            



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

          



  

  

               

    





            

              



           

             



  



     



        

                

            

        



      

                 

           

         







  

              

   

























 















































































































































   











































               

           

   



             



             











 













[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

             

  









prime ideal









  



           

 

          









prime ideal







 







prime ideal









       









prime ideal















        

        







   



    

   















              

      











   

     









       





 

















     



















 













     









            

                  

  







 







  







      



















 



 



 



   







     































             



      

 



                   

    



   



        



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

  

















    







  







       

 

           















 

























   







        



 















      















 













         



 







    

          



































     



         

  







          

    

















                

 



















 











       















     



  

    



  







  

                

                

 

  



           

 











  





         



     



 







  

     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

          









prime ideal









 



       

             

                  











     



        

       



         

        

               

               







  

 

 

1.3.3 Geometry of numbers

               

                

            

           

 











            











             













   

   



        



    















       



















 













      







 





















              

         

 



    

       



        

             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

𝐷

𝑒

     



    

 







 



  



























  

















    



         

                

        



      

          

                   

     

        







 

            

          







      









          







    





























          







 



























 

























             



 







[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

             



 

         

      

























              

































      



        









































        

             











  



      

                

                

         

   



    



   



     

  











  







     





                









      

























  



  

      





         

     

       

















 















  

















                 

     

































































































































































































             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

              

      

   









   







        

       



   

    



       

          







  









 

    





   

    

               



     

            



   

    



          

        



 



    

 



 



           

   





             









    



















          









      



























































 

           



















 















   

             









   

          



        

   



               



                 





             

     







  



    



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                    

    



              

 



             



             

             

              



  







             













          



   

















       



      









                  

 

              

        







 



















 







      















   

            

   







 



















    



    



   



























       



















     



      



















             

 



        

         

                

            

       



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

          

       









   































        



         

               

           

               

            

            

            

                 

       













 

          



        

                

       





















 

















          

  























































          



     









             







 

     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

ႼႵᆡ

ႼႴᆡ ႼႳᆡ

ႼႲᆡ Ⴒᆡ

Ⴓᆡ Ⴔᆡ

Ⴕᆡ

ႼႴᆡ

ႼႳᆡ

ႼႲᆡ

Ⴒᆡ

Ⴓᆡ

Ⴔᆡ

Ⴑ

ᆂ

           

;

0 + ℤ = 1 + ℤ

                      

 





      

















           

              

               

              

              

             

                  

              

                 

    



  

                 

                 

         



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

         

              

 





          



                

 



             

      

     















 

















                

              



   



























































         























      

             

          





















[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

              

















       



    

           

          

      







       

 







  















     













      













        













           















       











 





















              



 

      



         



   

    













    

















  







     



     













 

  

       







             







   

      







     







 















 

              

   



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                   

               

               



     

   







  











   







        



 

         











   









            

 



























































    



























  

















          













   



   















   











































































































































































   





























































      



 



        

      











      







 





















[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

        









































































   

































       







        













     

    











     





























































 

                 

           

 













  



 



     







  























 



   



















   



  



 



       















      















          

1.3.4 Absolute values and local ﬁelds

              

               

                 

            

      

    



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

   

    

 

       

       



     



               





    



  



   

            

       



 



   









         



  



    

           



























 





          



                 

                  

                 

             



     

        



        

    



             

          













                  

             

               

              

               

           

             

    

























   















    

 







          



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

                 

    







      











































   



            

             







  









      







    

             

          

                

                  

               

              

  

 

 

             

            







  

       







































   







     







  











       



































    

              

 



          

        







   



  























                 





           



 







        

 















  

























      

           



 

         







      















[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

    

 







           

 

     









        



   

           



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

2 Hilbert’s tenth problem

2.1 Diﬀerent perspectives on an old problem

2.1.1 Diophantine equations and sets

              

        

    

                

               

   

        

           

              

           



        











 







          









                  

                

        

      

                   

                   

      

     







      



  1  

    0 

              

      1  0         

        

                









   1      0 

 

             

               

                   

   

      



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

                

 α  α            

     



           

 















          





           

















   



              

 



              

          



     

     















  

 









  

























  







       









  









     



       







 









  

























                

 

             

  

   



      

   







          

           

           



   







 

            



  











               

              

   









     

           







 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

      

𝑥

+ 𝑦

= 1

−1 ≤ 𝑥 ≤ 1

         

  



      



























      











    











 

              







  











       



      











 

 



            

  





                 

 



            

    

        







 









 







 











              

   

























  

























          









 







     





 



 



 





    





 







[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

      







       



 



                 

      

  

                

               

           

           

                   

    



            

           

     











        

       





















 

















 

































 





















 



   







  



 



        







 





  



 



     



















   

































































    















    



 



    



















































            

        

  







































               

               

  



        

















 









  

























                  



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

      















































































           

                



















   



 



        



















               

   



 



    































































































































        













































































































































































           







    











               

             



  



          



 x

x

y

y

 









  y

y









y

y





      















        

      



















[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

                

                

                

         H10      

     

     H10

               

     

             

  







   









 









               

       



 





            

             

   



   

  

















 

















  

 



 



          







  

       







 





      

 



             













    



 



   



























              

       



















          







  

         

























   



  



    



   

 









































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

      

     







 







  



 





    









 

















 







 















































































             







 





 











































































                  

  

             

             

            

              

               

      

  



         

       









           





        



 











             

              

              







          



  





    H10

             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

                

          







   

               

 

2.1.2 Purely Diophantine sets

          



     

   















 

 









  

























          

              

               

         

             



  



           



 x

x

y

y



 









  y

y









y

y





               

               

                 

                 

            



   

               

              









               

          

   













           

             

       

                

         

              

                 

           



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

      

           

                 

         





  



   

     



 



        





 





  















   





             

   

              

             

 







     







    





            



 

    



           













    



          

             

      











  







 

   

       



   



















      

















      

  









                 

       











     



  







      



 

               

            

         



             

         

      



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

   



              







             

  







     







   

          

  



















        

 









  





























             

  

                  

  



   







 

    



     















 



 

      



     

         



  















           



    

          



   







   

 



 

  

















                

  



  





















        

















































































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

      

           





  





     



         

            















                 

    



  



    



    























     









 

             

        

                 

H10







            

H10

∗

(𝔒

𝐾

)

∃+

(𝔒

𝐾

)

Th(𝔒

𝐾

)

𝐷(𝔒

𝐾

)

H10(𝔒

𝐾

)

𝐷

∃+

(𝔒

𝐾

)

𝐷

𝑐

(𝔒

𝐾

)

𝒦

2.1.3 Related problems

                 

               

              

Th     

         

               

           



    

     Th



        

             

                   

             



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

            

 

             

     

                 

            

         H10    

   

               

           

  







































  













































              

   



          

      

       



    

             

           













   

  





















       





y

y





y

y

 

   H10         

        H10

     H10    

                 

                 

                 

               

                 

                

               

                





[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

                

       

 

  





   

              

    

               

 

2.2 Some structural results

              

              

 

   







         



  

  





   



 



     



  

  



  



        



  

     





  







       



 



  







  



     























            

    





















 











      





              

                

   

             

            H10 

   

             

            

          

                  

           

            













 

  



















 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

             

     H10

      



         





                  

  



       



       

    

               

    



           

 H10







 





                   





              

           

     



         

             















               

 H10







        

                

        

 

         



      

   



          

 





   





  



       101

         



 







-times



  





-times

 

               





       





 





   













     



   

        























































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

                

     



    



   





            





















































   





















































































































         



     

                 

 





                 

            



   

     



           

             

      



 



      

              

                    

           

            































   





















   

  



 

 







         







                

            



    



  



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

  



















      







































    



       

       

            







   

    



     

















 











  

   







   







     





















  





















 































      

















             









       













       







  

   







    























































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

  









                   

               

   

    



































        



        

       



         

   













    



  

















 



      





  



































 























        





  











      









  



























     

        





































     





































     



         



  









[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

  





      



































      







  



      

   



  















 







        

  

   

 

 



                

              

   





              

        



    

  

 



    















 























      



      



  







  

     































































                 

  



































































                 

   



         

















      







         



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

              

2.3 Hilbert’s tenth problem over totally real number ﬁelds and

number ﬁelds with one pair of non-real embeddings

                 

                

              

                

                  

             

2.3.1 Finitely many easy lemmas

           









 

               

    



  

 

       



       





  







      

    











 













 

    











 

      

                

 















      



    

 



 



          

 



               

   



 





               

  





 





 



  

   















      

      



       











 

   



             

  











 



         

    











[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

 







    

 













   

















  



          





























































even































odd





















    













even

































odd





















               

     

         



   

     



      













 

 







        



 

    







 

           



 



   

           







      

  







 























  















































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

     







































 

  

























         











 



     



            

        











        



 



  

 

         



    

  

 











 











   

 























  





















         













  



















 

   



 











  











  



  

      



 



 





































































 

















































   



 



 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

       















 











 

             



          



         

   

 



 



 





 

























 



   

    



 



    



  

                 



















              







 







  

 









     







































































odd



























          





   











 

    









 

  







        



















       







        

                

 



 



             

           

        



      

     

















 





















 











[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

         



      

      

















 





























 













  











 













         

        



     

     





 



 

     







  







 

               

  



         



 





                

   

        













 

 

            



 



  

           

























 

  



 

        



     

       



















             



 





    























































































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

             

                 

     





          



         

       



















        

                

  









































































          



         













     



 





              



  

  



      







  



   









 



 















 



       



       



 





           







    

  



          



  



 







        



     











       





          











  



 



  

   



 





         





























        



























[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   



          

     







































































   









   













































































































































           

            

















   





    











 



  



      











     



 







  







  









  



  







       

          

   

  



         













   













     













-times

    











 























      



 



 











      

















              

     













 

                

  

     



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

              

               

     





  





  

                 

                

                

             

           

             

             

           

2.3.2 Diophantine deﬁnition of over 

                  

              

     



         



   

               

        



     



    



 

           



    











     



 











       

     



       



 





      







        

     

            

























































 





















 

 







    

       



    







    

      



       



   









    

              





            

 

 

 







[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

         



      

    



  



         









 



     



  

         



   





















          



     

 



 



        





 





  

























 





























  



  

        



    



  

            



   

  

  



  



 



    

  



     

           



    

       







     

      



       

 



 



             

  



 



     





 



 

 











 



          

  

            



   

   



          

 











  

 



 



    



 

 







 





                  

          































































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

  



   



      



  

   



    



      





 



           

       









               

   

           



   

    

 









 







 



 







 

 









          







 





         



 

       







  







  

        

                

  

  







        

































       



      



     















           



   









  







      

            



  

       

 











 





 



 





  



 



 



 







  

        



















 





      

      







 





















































































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

     



   



























        



 



          























































      





















   

                   

      



    

               

      

     



             





















   







 







   































































  



 







   











 

















































  



















   







          

















[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

    

   













































    

















































               















by (iv)

 

        















         







 

     







      

        

         

     

     



           

              









                  



             



 

   



        





      





               

            



     



            

   





          



     

    

         



    





          











     









 





























[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

          









 



























  



  



  





   













  











       





  



     

  





























  















   

    

































































  





             













































         



















































































































 

      

































































































































         



    

           





               













[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

 



    





















    

       











     











 





















        





 













  











 

  

 





























































 



       







       

    



    











     

   



     



      



   







 







         

             





  











           



    



 





                   

                 

                

     

              





      







     





















 

    



      











       

             

        



  













   











































   















      



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

         



       

        









































          









even





































odd



























           







 









          



    

 











      





       



  







   



























































 



   







     







  



    

  

         



     

       







    





























 





            



 



 

                   



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   













 













 

















      

















    

      



     



 









 



 

        

 

















              

 



   







 



 



























  















        

     



























  















    



 





























                 

   















































































































            

     

 











  







 



   



  

   















 



























   



  





























[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

      



 











      





































       



















     



 

   

























































































         

      



 















     





  











      



    

         



   

















   

             





   



  



 



           









 







   







  















 

 







































   



      









































  



 











  



     























































































 















  



 













      

























































































































































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   































  



      

















  







 







        



  































   

            



   



          







   

    































        

 







  

 









 



 





         



         

              



 



 

   





































































































































































              



 





  































        







  





























































































































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18











































      





        

















 

 







         

  









Lem. 2.3.3.(ii)

 

















   







 















  

   



 



        









       







    

  

        









 



       

                 





































even































odd

























  



 



      



























   



 



  





          





            



  





























   



  









  















 



   

  







   







 







    

    







   

























  

























        











 



     













   







    







 











   



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

  





























     







  

















         

  









































































































































             





   

    











          













































































































    















































































































































































      



  



















     









































   



         

























































































 

       



   













































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

         



























             



  

  



  





 





















     





  



























































































































































































       







     



  

   



 









         























    

       







 











      

       











 







      

     











 























   

    















































































 







         















































































 









            



   

  







   







      

  





  



 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

  







  



 







  



 

             



 



























































              



 





    























   











 



       

         







 





            























































  



              

































          

   







 







        









              

    







   



  













































        









      



















































































 



  



 



  



    

    



 































































   



          



  









     



       















































[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

  













































      



         









 







  



  

               





            



 

 







          



    

   



             

               





 

  











































































































































































  



 





 









  



 

 





 

    

  

  



















 

             

              



   

      

                

      



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

             

                 

                





 



       



 





          



       

   





















































 























  



           





           

 

               

 





 









 









 









 





         









 













  



 





 











 

 



  



 









 



 





 



 

       





 

    





 





          

 



 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

            









 





    









 





         



      

  

            





  



           

 





        

 





        

























           





























               

          



 

             

















 







         



 



           



 





























[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

      



 



      

 





  















    

 

  





  

      



 



     











   









     



 



   

              



  







 





             



  









 



      







 



 

   



 



 







       

  



       









 







           

        

                 

            





           



       

           































































               



               

              

                

               

              



               

               

                

         

               

   



          

           

             

  H10



           

             H10



  

                

               



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

A Appendix

A.1 Collected Haskell implementations

A.1.1 Simulating Turing machines

            https://github.com/

tim6her/h10-turing-machines              

 

git clone https://github.com/tim6her/h10-turing-machines.git

cd h10-turing-machines

cabal setup && cabal build && cabal install

              ghci  

              

             

>>> import Automaton.TuringMachine

>>> :l tally

>>> let d = toTransition tally "error" -- mark the errornous state

>>> let turing = TuringMachine "start" '_' "halt" d

>>> "§1111" >>> turing -- Tally encoding of 4

Just "§1"

>>> "§1011" >>> turing -- Not tally encoded

Just "§0"

             

A.1.2 Polynomials

              

             

        

          

{-# LANGUAGE RebindableSyntax #-}

module Monomial

( Monomial

, (<*>)

, idt

, mfromList



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

 

, clean

) where

import NumericPrelude

import Data.Map (Map, delete, empty, foldrWithKey, fromList, member, insert,

insertWith, (!))

import Algebra.Monoid as Monoid

import Test.Tasty

import Test.Tasty.HUnit

import Test.Tasty.QuickCheck as QC

-- | Monomials are mappings from ZZ to NN with finite support

newtype Monomial = Monomial (Map Integer Integer) deriving (Eq, Ord)

instance Monoid.C Monomial where

idt = Monomial empty

(<*>) = mmul

instance Show Monomial where

show (Monomial m)

| m == empty = "1"

| otherwise = foldrWithKey

(\x e sh -> "X" ++ show x ++ "^" ++ show e ++ " " ++ sh)

"" m

-- | Creates monomials from list of tuples

-- Left entry is index of indeterminate, right index is power of the

-- indeterminate

-- === Example

-- >>> mfromList [(1, 2), (0, 3), (4, 7)]

-- X0^3 X1^2 X4^7

mfromList :: [(Integer, Integer)] -> Monomial

mfromList l = clean $ Monomial $ fromList l

-- | Multiplies two monomials

-- === Example

-- >>> mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])

-- X1^2 X2^5 X3^2

mmul :: Monomial -> Monomial -> Monomial

mmul xx@(Monomial m1) yy@(Monomial m2)

| m1 == empty = yy



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

| m2 == empty = xx

| otherwise = clean $ Monomial $ foldrWithKey

(\x e m -> if x `member` m

then insertWith (+) x e m

else insert x e m)

m2 m1

clean :: Monomial -> Monomial

clean (Monomial m)

| m == empty = (Monomial m)

| otherwise = Monomial $ foldrWithKey

(\x e m -> if e <= 0

then delete x m

else m)

m m

-- * Testing

main :: IO ()

main = defaultMain tests

tests :: TestTree

tests = testGroup "Tests" [properties, unitTests]

properties :: TestTree

properties = testGroup "Properties" [qcProps]

qcProps = testGroup "Axioms of monoids"

[ QC.testProperty "left multiplication by identity" $

\x -> (let m = mfromList (x :: [(Integer, Integer)])

in idt <*> m == m)

, QC.testProperty "right multiplication by identity" $

\x -> (let m = mfromList (x :: [(Integer, Integer)])

in m <*> idt == m)

, QC.testProperty "associativity" $

\x y z -> (let m1 = mfromList (x :: [(Integer, Integer)])

m2 = mfromList (y :: [(Integer, Integer)])

m3 = mfromList (z :: [(Integer, Integer)])

in (m1 <*> m2) <*> m3 == m1 <*> (m2 <*> m3))

, QC.testProperty "commutativity" $

\x y -> (let m1 = mfromList (x :: [(Integer, Integer)])

m2 = mfromList (y :: [(Integer, Integer)])

in m1 <*> m2 == m2 <*> m1)

]

unitTests = testGroup "Unit tests"



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

 

[ testCase "show X0^3 X1^2 X4^7" $

show (mfromList [(1, 2), (0, 3), (4, 7)]) @?= "X0^3 X1^2 X4^7 "

, testCase "sample multiplication" $

show (mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])) @?=

"X1^2 X2^5 X3^2 "

, testCase "test clean" $

mfromList [(1, 0), (2, 0), (3, 1)] @?= mfromList [(3, 1)]

]

          

{-# LANGUAGE RebindableSyntax #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE MultiParamTypeClasses #-}

import NumericPrelude

import qualified Monomial

import qualified Data.Map as Map

import Algebra.Monoid as Monoid

import Algebra.Ring as Ring

import Algebra.Module as Module

import Algebra.Additive as Additive

import Test.Tasty

import Test.Tasty.HUnit

import Test.Tasty.QuickCheck as QC

-- | Polynomials over a ring R are finitely supported functions

-- from the set of monomials to R

newtype Polynomial a = Polynomial (Map.Map Monomial.Monomial a)

-- | Polynomials form an additive (abelian) group

instance (Ring.C a, Eq a) => Additive.C (Polynomial a) where

zero = Polynomial Map.empty

(+) = padd

negate (Polynomial m) = Polynomial $ Map.map negate m

-- | Polynomials from an R-module

instance (Ring.C a, Eq a) => Module.C a (Polynomial a) where

(*>) 0 _ = zero

(*>) a (Polynomial m) = Polynomial $ Map.map (a*) m

-- | Polynomials form a ring with unit

instance (Ring.C a, Eq a) => Ring.C (Polynomial a) where

one = pfromList [(1, [])]

(*) p@(Polynomial m1) q



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

| p == zero = zero

| q == zero = zero

| p == one = q

| q == one = p

| otherwise = Map.foldrWithKey

(\mono coeff poly -> (coeff *> mono `mmul` q) + poly)

0 m1

-- | Two polynomials are equal if their difference is zero

instance (Ring.C a, Eq a) => Eq (Polynomial a) where

(==) p q = let (Polynomial m) = p - q in m == Map.empty

instance (Show a, Eq a) => Show (Polynomial a) where

show (Polynomial p)

| p == Map.empty = "0"

| otherwise = Map.foldrWithKey

(\m a sh -> show a ++ " " ++ show m ++ "+ " ++ sh)

"" p

-- | Adds two polynomials over the same ring

-- If a coefficient of a monoid equals 0 the monoid is dropped out of the map

padd :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a -> Polynomial a

padd p@(Polynomial m1) q@(Polynomial m2)

| m1 == Map.empty = q

| m2 == Map.empty = p

| otherwise = clean $ Polynomial $ Map.foldrWithKey

(\mono coeff poly -> if mono `Map.member` poly

then Map.insertWith (+) mono coeff poly

else Map.insert mono coeff poly)

m2 m1

mmul :: (Ring.C a, Eq a) => Monomial.Monomial -> Polynomial a -> Polynomial a

mmul mono poly@(Polynomial mp)

| mono == Monomial.idt = Polynomial mp

| poly == zero = zero

| otherwise = Polynomial $ Map.mapKeys (mono Monomial.<*>) mp

-- | Generate polynomials from lists

pfromList :: (Ring.C a, Eq a) => [(a, [(Integer, Integer)])] -> Polynomial a

pfromList [] = zero

pfromList ((a, m):l) = deepClean . clean $ (Polynomial $ Map.singleton

(Monomial.mfromList m) a) + pfromList l

-- | Comfort function for creating polynomials



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

 

-- === Example

-- >>> 2 *> ((x 1 + x 2) * (x 1 - x 2)) == 2 *> x 1 ^ 2 - 2 *> x 2 ^ 2

-- True

x :: (Ring.C a, Eq a) => Integer -> Polynomial a

x i = pfromList [(1, [(i, 1)])]

-- | Remove monoids with coefficient zero from support

clean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a

clean (Polynomial m) = Polynomial $ Map.foldrWithKey

(\mono coeff poly -> if coeff == 0

then Map.delete mono poly

else poly)

m m

-- | Remove variables with power zero from monomials

-- This function runs in O(n log(n)) so use it sparsely

deepClean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a

deepClean (Polynomial m) = Polynomial $ Map.mapKeys Monomial.clean m

-- * Testing

main :: IO ()

main = defaultMain tests

tests :: TestTree

tests = testGroup "Tests" [properties, unitTests]

properties :: TestTree

properties = testGroup "Properties" [qcAddProps, qcModProps,

localOption (QuickCheckTests 5) qcRingProps,

qcAlgebraProps]

qcAddProps = testGroup "Group axioms for addition"

[ QC.testProperty "addition is commutative" $

\x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

q = pfromList (y :: [(Int, [(Integer, Integer)])])

in p + q == q + p)

, QC.testProperty "addition is associative" $

\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

p3 = pfromList (z :: [(Int, [(Integer, Integer)])])

in (p1 + p2) + p3 == p1 + (p2 + p3))

, QC.testProperty "addition by zero" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

   

in p + zero == p)

, QC.testProperty "addition with inverse" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in p - p == zero)

]

qcModProps = testGroup "Module axioms"

[ QC.testProperty "first distributive law" $

\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

q = pfromList (y :: [(Int, [(Integer, Integer)])])

in (a :: Int) *> (p + q) == a *> q + a *> p)

, QC.testProperty "second distributive law" $

\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in (a + b :: Int) *> p == a *> p + b *> p)

, QC.testProperty "multiplications commute" $

\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in (a * b :: Int) *> p == a *> (b *> p))

, QC.testProperty "multiplication by one" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in (one :: Int) *> p == p)

]

qcRingProps = testGroup "Ring axioms"

[ QC.testProperty "multiplication is associative" $

\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

p3 = pfromList (z :: [(Int, [(Integer, Integer)])])

in (p1 * p2) * p3 == p1 * (p2 * p3))

, QC.testProperty "left multiplication by one" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in one * p == p)

, QC.testProperty "right multiplication by one" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in p * one == p)

, QC.testProperty "distributive law" $

\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

p3 = pfromList (z :: [(Int, [(Integer, Integer)])])

in p1 * (p2 + p3) == p1 * p2 + p1 * p3)

]

qcAlgebraProps = testGroup "Algebra axioms"

[ QC.testProperty "multiplications commute" $

\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

 

]

unitTests = testGroup "Unit tests"

[ testCase "sample polynomial" $

show (pfromList [(1, [(1, 2), (3, 4)]), (-4, [(1, 4), (2, 3)])]

:: Polynomial Int) @?= "1 X1^2 X3^4 + -4 X1^4 X2^3 + "

, testCase "test equality" $

pfromList [(0, [(1, 1)])] @?= (zero :: Polynomial Int)

]



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

Bibliography

          

         

             

       http://www.jstor.org/stable/2269326

             

       10.2307/2371045

       

 

      

         10 . 2307 / 2318447 

http://www.jstor.org/stable/2318447

              

        10.1016 /j. amc.2005. 09.066 

https://doi.org/10.1016/j.amc.2005.09.066

            

           

            

           

               

      10.2307/1998133

               

      10.2307/2040720

                

           10.1112/jlms/s2-18.3.

385

                

        10.1515/crll.1988.388.189 

https://doi.org/10.1515/crll.1988.388.189

             

      10.1112/jlms/s1-8.1.18

               

     

 



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18



            

            

           

             

10.1007/BF01700692  https://doi.org/10.1007/BF01700692

             

     

             

             

10.1090/S0273-0979-00-00881-8

     

         

    

          

           

        10.1007/978- 3- 642-

75306-0

           

              

          

              

   10.1215/S0012-7094-36-00227-2  https://doi.org/10.

1215/S0012-7094-36-00227-2

           

           

          

  10.1007/978-3-642-54936-6_5

            

       10.1007/978-1-4613-0041-0 

https://doi.org/10.1007/978-1-4613-0041-0

             

  

              

             https://

www.ebook.de/de/product/3665990/david_marker_model_theory_an_introduction.

html

            

       

           www.jmilne.org/

math/



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18



           

    http://www.logic.univie.ac.at/~muellem3/TCS.pdf  



        

    

               

          http : / / ubdata .

univie.ac.at/AC05622932

               

           10.4310/MRL.2013.v20.

n5.a12

               

          10.2307/2047021 

https://doi.org/10.2307/2047021

            

          http://www.ams.org/

notices/200803/tx080300344p.pdf

            

        

           10.1007/3 - 540-

45455-1_4

             

            10.1090/S0002-

9904-1944-08111-1  https://doi.org/10.1090/S0002-9904-1944-08111-1

             

          10.2307/2266510

              

        10.2307/2033628  https://doi.

org/10.2307/2033628

            

        10.2307/2266685

              

      10.2307/2269028

               

        10.1515/crll.1986.368.127 

https://doi.org/10.1515/crll.1986.368.127

          

              

 10.1002/cpa.3160420805  https://doi.org/10.1002/cpa.3160420805



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18



           

             10 .

1002/cpa.3160420703

            

            

           https://doi.org/

10.1090/conm/270/04370

           

            

     http : / / www . ebook . de / de / product / 6433593 /

alexandra_shlapentokh _hilbert_s_tenth_problem_diophantine_classes_and_

extensions_to_global_fields.html

          http://math.

cornell.edu/~shore/papers/pdf/proc4t.pdf   

              

               

        10.1016/S0049-237X(99)

80028-7 http://www.sciencedirect.com/science/article/pii/S0049237X99800287

            

      http://eudml.org/doc/212515

            

             

10.1112/plms/s2-42.1.230  https://doi.org/10.1112/plms/s2-42.1.230



[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18

Todo list

                                        

                                          

                                     

                                     

                                       

                                       

                                           

                          

